module Politics

abstract sig Document{ }
abstract sig Photo{ }
abstract sig Word{}
abstract sig Accepted{}
abstract sig Yes, No extends Accepted{}

sig User{
	id: one Int,
	name: one Word,
	surname: one Word,
	email: one Word,
	password: one Word,
	dateBirth: one Int,
	vote: lone Vote
}

one sig Governor extends User{
	election:one Election,
}

sig Candidate extends User{
	cv: one Document,
	motLetter: one Document,
	party: one Party,
	dateCand : one Int
}{cv !=motLetter
	dateCand > Election.startCandidacy
	dateCand < Election.EndCandidacy}

sig Member extends Candidate{
	status: Yes
}
sig Election{
	startCandidacy:one Int,
	EndCandidacy:one Int,
	dateElection: one Int
}{startCandidacy < EndCandidacy
 	dateElection>EndCandidacy}

sig Party{
	id:one Int,
	name:one Word,
	program:one Document,
	symbol :one Photo,
	DateCreate: one Int
}{DateCreate>Election.startCandidacy
	DateCreate<Election.EndCandidacy}

sig Vote{
	dateVote: one Int,
	preference1: one Candidate,
	preference2: lone Candidate,
	preference3: lone Candidate
}{preference1 != preference2 
 	preference1 != preference3
 	preference2 != preference3
 	dateVote = Election.dateElection}

// Facts
// Every user has a unique ID and username
fact noTwoUsersWithSameID{
	no disj u1, u2 : User | u1.id = u2.id || u1.email = u2.email
}

// Every party is unique, with unique name, program and symbol
fact noTwoSameParties{
	no disj p1, p2 : Party | p1.name = p2.name || p1.program = p2.program || p1.symbol  = p2.symbol
}

// Every candidate has a unique cv and motivation letter
fact noTwoSameCandidates{
	no disj c1, c2 : Candidate | c1.cv = c2.cv || c1.motLetter = c2.motLetter
}


// All preferences in the vote are on the same party
fact AllPreferencesSameParty{
	all v: Vote | v.preference1.party =  v.preference2.party and  v.preference1.party =  v.preference3.party
 }

// One user can vote only once on an election
fact OneUserOneVote{
	no disj v1, v2:Vote |one u:User | u.vote = v1 and u.vote = v2
}


assert NoSameUsers{
	no disj u1, u2 : User | u1.id = u2.id || u1.email = u2.email
} 


//check NoSameUsers for 4

pred show()
{
	#Election > 1
	#Party > 5
	#Candidate > 8
	#User > 10
}


run show for 8
